This invention relates to a method of analyzing a circuit having at least one structural loop between different channel connected components within the circuit, especially, though not exclusively, for use in Computer-Aided Design (CAD) tools for Electronic Design Automation (EDA), and more particularly for deriving equivalent behavior of mixed (gate and switch) level digital circuits.
Contemporary chip design depends critically on the availability of appropriate EDA CAD tools in order to keep up with the ever-increasing chip complexity. Designers typically work with chip descriptions at several levels of abstraction. The Register-Transfer Level (RTL) describes a circuit at the high level of boolean functions and data flow within the circuit much like a regular programming language does. Gate-level descriptions provide a structural (schematic) description of a circuit as an interconnection of basic blocks called gates, whereas every gate has a known and relatively simple boolean behavior. Switch-level descriptions represent the lowest level of circuit design abstraction which again is a structural (schematic) one and contains an interconnection of switches (transistors) that implement the desired functionality of the circuit.
RTL is often the preferred abstraction level for most design activities, however, any RTL design has to be translated into an equivalent switch-level design as a necessary step prior to the fabrication of the chip. This translation can be performed using so-called synthesis EDA tools that compile RTL designs into a predefined, technology-specific gate-level cell library that contains a switch-level schematic for each cell. In some cases, especially when a chip has to meet stringent operating requirements (speed, power consumption, etc.), certain blocks of the chip may be designed at the switch level.
For a number of reasons, it is highly desirable and advantageous to accurately translate the functionality implemented by a circuit description containing switches into a higher level (gate or RTL) one. A very important application of such a technology is formal functional verification of circuits. Formal functional verification aims to ensure that a chip operates as expected based on appropriate mathematical models. Unlike traditional functional verification approaches, such as simulation, formal verification provides 100% coverage of a circuit""s functionality. To enable formal functional verification at the mixed (switch and gate) level, a method is required to translate the structural description of a circuit into a functional (boolean) description in the corresponding mathematical model. Other application areas for mixed (switch and gate) level circuit analysis and translation include technology-specific library characterization, Automatic Test Pattern Generation (ATPG), and re-synthesis and re-design of chips from one chip manufacturing technology to another.
Various techniques have been developed for the analysis of the behavior of mixed (switch and gate) level circuits. These techniques process the circuit in parts called Channel Connected Components (CCC). A CCC comprises of transistors that are electrically connected to each other via their channel terminals and other transistors in the CCC, and gates connected to the channel terminals of any transistor in the CCC. The CCCs in a circuit can be analyzed one at a time; there are known techniques that can accomplish that based on explicit or implicit conductive transistor path enumeration. Individual CCC behavior is then composed to obtain the behavior of the complete circuit.
Thus, a key aspect in deriving a functional model of a complete circuit is the ability to identify and properly characterize the behavior introduced by structural dependency loops between two or more CCCs in the circuit. Structural loops may result in combinational, sequential, or oscillatory behavior. Existing approaches either represent this behavior at a very low level or completely ignore the problem. For example, the ANAMOS and TRANALYZE tools, as presented in the article xe2x80x9cBoolean Analysis of MOS Circuitsxe2x80x9d by R. E. Bryant published in IEEE TCAD, 6(4), pp. 634-649, July 1987, and later refined in the article xe2x80x9cExtraction of Gate-Level Models from Transistor Circuits by Four-Valued Symbolic Analysisxe2x80x9d also by R. E. Bryant and published in ICCAD ""91 resolve structural loops between CCCs by inserting a unit delay element into the loop. The derived circuit model therefore contains an extra inputxe2x80x94the so-called xe2x80x9csimulation clockxe2x80x9d, and is likely to contain many more state-storing elements than the original gate/RTL level design. These tools were developed at the Carnegie Mellon University for the purpose of transistor-level simulation and mapping into a hardware-based gate-level simulator and derive models of the circuit that are not directly suitable for obtaining an RTL description similar to the desired design. This essentially prohibits the interaction of ANAMOS and TRANALYZE with the majority of the currently available EDA CAD tools. Furthermore, the method for deriving a circuit description suitable for formal verification and/or resynthesis from the model produced by ANAMOS and TRANALYZE in the article xe2x80x9cComparing Layouts with HDL Models: a Formal Verification Techniquexe2x80x9d by T. Kam and P. A. Subrahmanyam published in IEEE TCAD, April 1995, pp. 503-509 involves an elaborate and computationally intensive process which is not suitable for circuits of any practical size.
Another approach to mixed (gate and switch) level circuit analysis has been implemented in the Verity tool developed by International Business Machines Corporation, and described in the article xe2x80x9cVerityxe2x80x94a Formal Verification Program for Custom CMOS Circuitsxe2x80x9d by A. Kuehlmann, A. Srinivasan and D. P. LaPotin published in the IBM R and D Journal, Vol. 39, pp. 149-165, January-March 1995. This tool is a logic checker capable of working at the switch level. It only goes as far as analyzing if a structural loop of CCCs results in combinational or sequential behavior. In the latter case, the user is informed of the presence of a non-combinational loop and circuit analysis is aborted. Furthermore, the technique fails to properly recognize combinational loops in some cases. The tool does not output an equivalent higher-level model nor does it work directly on sequential designs.
The present invention therefore seeks to provide a method of analyzing a circuit having at least one structural loop between different channel connected components within the circuit, which overcomes, or at least reduces the above-mentioned problems of the prior art.
Accordingly, the invention provides a method of analyzing a circuit, the circuit having at least one structural loop between different channel connected components within the circuit, the method comprising the steps of:
at least partly notionally splitting the circuit into its constituent channel connected components;
detecting the at least one structural loop;
inserting a pair of temporary boolean variables at a break point on a boundary between different channel connected components to notionally break the at least one structural loop;
analyzing each channel connected component in the at least one structural loop utilizing the pair of temporary boolean variables at the break point in order to obtain a pair of boolean functions representing the functionality of the circuit at the at least one break point;
analyzing the pair of boolean functions, including determining whether the at least one structural loop is sequential in nature; and
modifying the pair of boolean functions when the at least one structural loop is sequential in nature in order to remove any dependence in the pair of boolean functions on the pair of boolean variables.
In a preferred embodiment, the method further comprises the step of utilizing the pair of boolean functions to produce an RTL description of the circuit in any desired RTL language. The circuit may include at least one transistor-level component and/or at least one gate-level component.
Preferably, the step of analyzing the pair of boolean functions comprises:
reformulating each of the pair of boolean functions to have at least a first term which is independent of both of the boolean variables, at least a second term dependent on one of the boolean variables, and at least a third term which is dependent on the inverse of said one of the boolean variables, wherein any of the terms may be zero;
determining whether the second term is non-zero and whether the third term is zero, in which case the at least one structural loop is sequential in nature.
The step of modifying the boolean functions preferably involves setting the second term to zero.
The step of analyzing the pair of boolean functions preferably includes determining whether the at least one structural loop is combinational in nature. This step preferably comprises:
reformulating each of the pair of boolean functions to have at least a first term which is independent of both of the boolean variables, at least a second term dependent on one of the boolean variables, and at least a third term which is dependent on the inverse of said one of the boolean variables, wherein any of the terms may be zero;
determining whether both the second and third terms are zero, in which case the at least one structural loop is combinational in nature.
The step of analyzing the pair of boolean functions preferably includes determining whether the at least one structural loop is oscillatory in nature and preferably outputting a signal indicating that the circuit includes an oscillatory loop when the at least one structural loop is oscillatory in nature. This step preferably comprises:
reformulating each of the pair of boolean functions to have at least a first term which is independent of both of the boolean variables, at least a second term dependent on one of the boolean variables, and at least a third term which is dependent on the inverse of said one of the boolean variables, wherein any of the terms may be zero;
determining whether the third term is non-zero, in which case the at least one structural loop is oscillatory in nature.
The step of analyzing the pair of boolean functions preferably includes the steps of:
determining a loop signature for the at least one structural loop by combing each boolean function when dependent on a different one of the pair of boolean variables having different bias values, so as to obtain a unique signature for each possible combination of terms;
determining whether the unique signature is one of a set of predetermined unique values; and
making each of the boolean functions dependent on only one of the boolean variables by replacing the other of the boolean variables by an inverse of the one of the boolean variables, when the loop signature is not one of the set of predetermined unique values.